/* testing lib function printp, printb, and print */
int * x;

/* result should be:
 * 0x0 0xadd1 0xadd1 25 true false
 * (and there is a \n between each pair of them)
 */
/*@*/
void main(){
  x = null;
  printp(x);
  x = alloc(int);
  printp(x);
  *x = 1;
  printp(x);
  
  print(25);
  printb(true);
  printb(false);
  return;
}
/*@*/
